*****∧I newaxiom;

1 ((a=a∨b=a)∧∀x.(x=a⊃isblock(x)))⊃∀x.(isblock(x)⊃x=a)  

*****ASSUME isblock(a);

2 isblock(a)  (2)

*****TAUTEQ x=a⊃isblock(x) 2;

3 x=a⊃isblock(x)  (2)

*****∀I ↑ x;

4 ∀x.(x=a⊃isblock(x))  (2)

*****TAUTEQ ∀x.(isblock(x)⊃x=a) 1,4;

5 ∀x.(isblock(x)⊃x=a)  (2)

*****∀E ↑ x;

6 isblock(x)⊃x=a  (2)

*****TAUTEQ isblock(x)≡x=a 2,6;

7 isblock(x)≡x=a  (2)

*****∀I ↑ x;

8 ∀x.(isblock(x)≡x=a)  (2)

*****⊃I 2⊃↑;

9 isblock(a)⊃∀x.(isblock(x)≡x=a)  

*****∧I newaxiom;

10 ((a=b∨b=b)∧∀x.(x=b⊃isblock(x)))⊃∀x.(isblock(x)⊃x=b)  

*****ASSUME isblock(b);

11 isblock(b)  (11)

*****TAUTEQ x=b⊃isblock(x) 11;

12 x=b⊃isblock(x)  (11)

*****∀I ↑ x;

13 ∀x.(x=b⊃isblock(x))  (11)

*****TAUTEQ ∀x.(isblock(x)⊃x=b) 10,13;

14 ∀x.(isblock(x)⊃x=b)  (11)

*****∀E ↑ x;

15 isblock(x)⊃x=b  (11)

*****TAUTEQ isblock(x)≡x=b 11,15;

16 isblock(x)≡x=b  (11)

*****∀I ↑ x;

17 ∀x.(isblock(x)≡x=b)  (11)

*****⊃I 11⊃↑;

18 isblock(b)⊃∀x.(isblock(x)≡x=b)  

*****TAUT ∀x.(isblock(x)≡x=a)∨∀x.(isblock(x)≡x=b) whichblock,9,18;

19 ∀x.(isblock(x)≡x=a)∨∀x.(isblock(x)≡x=b)  

*****ASSUME (P(a)∨P(b))∧∀x.(P(x)⊃isblock(x));

20 (P(a)∨P(b))∧∀x.(P(x)⊃isblock(x))  (20)

*****TAUT ∀x.(P(x)⊃isblock(x)) 20;

21 ∀x.(P(x)⊃isblock(x))  (20)

*****∀E ↑ x;

22 P(x)⊃isblock(x)  (20)

*****ASSUME ∀x.(isblock(x)≡x=a);

23 ∀x.(isblock(x)≡x=a)  (23)

*****∀E ↑ x;

24 isblock(x)≡x=a  (23)

*****ASSUME P(a);

25 P(a)  (25)

*****TAUTEQ isblock(x)⊃P(x) 22,24:25;

26 isblock(x)⊃P(x)  (20 23 25)

*****∀I ↑ x;

27 ∀x.(isblock(x)⊃P(x))  (20 23 25)

*****⊃I ↑↑↑⊃↑;

28 P(a)⊃∀x.(isblock(x)⊃P(x))  (20 23)

*****⊃I 23⊃↑;

29 ∀x.(isblock(x)≡x=a)⊃(P(a)⊃∀x.(isblock(x)⊃P(x)))  (20)

*****⊃I 20⊃↑;

30 ((P(a)∨P(b))∧∀x.(P(x)⊃isblock(x)))⊃(∀x.(isblock(x)≡x=a)⊃(P(a)⊃∀x.(isblock(x)⊃P(x))))  

*****ASSUME ∀x.(isblock(x)≡x=b);

31 ∀x.(isblock(x)≡x=b)  (31)

*****∀E ↑ x;

32 isblock(x)≡x=b  (31)

*****ASSUME P(b);

33 P(b)  (33)

*****TAUTEQ isblock(x)⊃P(x) 22,32:33;

34 isblock(x)⊃P(x)  (20 31 33)

*****∀I ↑ x;

35 ∀x.(isblock(x)⊃P(x))  (20 31 33)

*****⊃I ↑↑↑⊃↑;

36 P(b)⊃∀x.(isblock(x)⊃P(x))  (20 31)

*****⊃I 31⊃↑;

37 ∀x.(isblock(x)≡x=b)⊃(P(b)⊃∀x.(isblock(x)⊃P(x)))  (20)

*****⊃I 20⊃↑;

38 ((P(a)∨P(b))∧∀x.(P(x)⊃isblock(x)))⊃(∀x.(isblock(x)≡x=b)⊃(P(b)⊃∀x.(isblock(x)⊃P(x))))